|
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system〔R. W. Floyd. "(Assigning meanings to programs. )" Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.〕 for flowcharts. ==Hoare triple== The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form : ''C'' where ''P'' and ''Q'' are ''assertions'' and ''C'' is a ''command''.〔Hoare originally wrote "''P'' ''Q''" rather than " ''C'' ".〕 ''P'' is named the ''precondition'' and ''Q'' the ''postcondition'': when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic. Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Hoare logic」の詳細全文を読む スポンサード リンク
|